\begin{tabbing} (\=if (((first\_nat 2:n)) = 0) then (Repeat (((SplitOnConclITE) \+ \\[0ex]CollapseTHEN (Auto'))$\cdot$ \-\\[0ex])\=) else (RepeatFor (first\_nat 2:n) (((SplitOnConclITE) \+ \\[0ex]CollapseTHEN (Auto'))$\cdot$)))$\cdot$ \- \end{tabbing}